perm filename LISPAX.PPR[W82,JMC] blob
sn#640280 filedate 1982-02-04 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 [Lines in brackets are added to the proof printed by EKL].
C00014 00003 linenames:
C00016 ENDMK
C⊗;
[Lines in brackets are added to the proof printed by EKL].
the proof LISPAX:
[Three kinds of variables are declared. We haven't used the simple ground
variables yet].
(DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) |GROUND| VARIABLE LISTP)
(DECL (X Y Z) |GROUND| VARIABLE SEXP)
(DECL (A B C) |GROUND| VARIABLE)
[phi is used in induction axioms].
(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)
[Alas, EKL won't let us use NIL for itself].
(DECL (NNIL) |GROUND| CONSTANT LISTP)
[A leftover. We actually use the infix give next].
(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)
[We'd like to use . for cons, but EKL won't let us. Since we use ¬ for not,
~ is availabel for cons].
(DECL (~) |GROUND⊗GROUND→GROUND| CONSTANT NIL INFIX 850)
[Because car, cdr, atom and null are declared unary, their arguments don't
have to be enclosed in parentheses. Note the binding powers].
(DECL (CAR CDR) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(DECL (ATOM NULL) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
[LISTP is also used as a sort, but we need it as a predicate name].
(DECL (LISTP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(DECL (SEXP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
[Lists are S-expressions].
(AXIOM |∀U.SEXP U|)
12. ∀U.SEXP U
deps: NIL
This comment is generated by the LNAME "function" that puts the previous line
into the collection SORTINFO used for giving the sorts of expressions, so
EKL will substitute them for variables of the given sorts without generating
extra premisses].
(COMMENTL LNAME SORTINFO)
[consing an S-expression onto a list yields a list].
(AXIOM |∀X U.LISTP X~U|)
14. ∀X U.LISTP X~U
deps: NIL
[The previous line goes both into SORTINFO and SIMPINFO used for simplification].
(COMMENTL LNAME SORTINFO SIMPINFO)
[This one hasn't been used so far.]
(AXIOM |∀U.NULL U≡U=NNIL|)
16. ∀U.NULL U≡U=NNIL
deps: NIL
[This has been used a lot. It's the right form for simplification].
(AXIOM |NULL NNIL|)
17. NULL NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.SEXP X~Y|)
19. ∀X Y.SEXP X~Y
deps: NIL
(COMMENTL LNAME SORTINFO)
[In some sense, this is the first substantive axiom].
(AXIOM |∀X Y.¬ATOM X~Y|)
21. ∀X Y.¬ATOM X~Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
[The list form of the axiom is also used, but perhaps it's redundant].
(AXIOM |∀X U.¬NULL X~U|)
23. ∀X U.¬NULL X~U
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
[The two main algebraic axioms both for lists and S-expressions].
(AXIOM |∀X U.CAR (X~U)=X|)
25. ∀X U.CAR (X~U)=X
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X U.CDR (X~U)=U|)
27. ∀X U.CDR (X~U)=U
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.CAR (X~Y)=X|)
29. ∀X Y.CAR (X~Y)=X
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X Y.CDR (X~Y)=Y|)
31. ∀X Y.CDR (X~Y)=Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
[Induction takes the form of an axiom in EKL - not just a schema, since
type theory allows quantification over predicates].
(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))|)
33. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))
deps: NIL
(LINENAME LISTINDUCTION *)
(COMMENTL LNAME LISTINDUCTION)
(AXIOM |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))|)
35. ∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))
deps: NIL
(LINENAME SEXPINDUCTION *)
(COMMENTL LNAME SEXPINDUCTION)
[The "function" LIST has to be declared "functional" since it takes a variable
number of arguments. Unfortunately, its semantics has to be given by separate
axioms for each length of list that is to be used. Well anything is better
than writing a chain of conses].
(DECL (LIST) |(GROUND*→GROUND)| FUNCTIONAL)
(AXIOM |∀X.LISTP LIST(X)|)
38. ∀X.LISTP LIST(X)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X.LIST(X)=X~NNIL|)
40. ∀X.LIST(X)=X~NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.LISTP LIST(X,Y)|)
42. ∀X Y.LISTP LIST(X,Y)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.LIST(X,Y)=X~LIST(Y)|)
44. ∀X Y.LIST(X,Y)=X~LIST(Y)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y Z.LISTP LIST(X,Y,Z)|)
46. ∀X Y Z.LISTP LIST(X,Y,Z)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)|)
48. ∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)
deps: NIL
(COMMENTL LNAME SIMPINFO)
[The infix * is used for append. Moreover, we declare it associative,
so the proof of its associativity is trivial now, and no statement of
its associativity has to be used in proofs of other facts.]
(DECL (*) |(GROUND⊗GROUND*→GROUND)| FUNCTIONAL NIL INFIX 840 BOTH)
(AXIOM |∀U V.LISTP U*V|)
51. ∀U V.LISTP U*V
deps: NIL
(LINENAME LISTAPPEND *)
(COMMENTL LNAME SORTINFO LISTAPPEND)
(AXIOM |∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)|)
53. ∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)
deps: NIL
[Recursive definitions are included in the line-name collection DEFINFO. They
have to be used discreetly in rewrites or they'll cause indefinite rewrites
causing EKL to run out of PDL].
(COMMENTL LNAME DEFINFO)
[We begin some facts that are easily proved but convenient to have on hand.
These axioms are intended to be convenient for proving substantial facts
about LISP programs rather than to be logically minimal].
(AXIOM |∀U.NNIL*U=U|)
55. ∀U.NNIL*U=U
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(AXIOM |∀X U V.X~U*V=X~(U*V)|)
57. ∀X U V.X~U*V=X~(U*V)
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
[alists deserve more special axioms than we have given them so far].
(DECL (ALIST A0 A1 A2) |GROUND| VARIABLE ALISTP)
(DECL (ASSOC) |GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN NNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALIST ELSE ASSOC(X,CDR ALIST)|)
61. ∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN NNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALIST ELSE ASSOC(X,CDR ALIST)
deps: NIL
(COMMENTL LNAME DEFINFO)
(DECL (MEMBER) |GROUND⊗GROUND→TRUTHVAL| CONSTANT)
(AXIOM |∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))|)
64. ∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))
deps: NIL
(COMMENTL LNAME DEFINFO)
[Perhaps we'll purge reverse later as not important enough for the basic function
list].
(DECL (REVERSE) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(AXIOM |∀U.LISTP REVERSE U|)
67. ∀U.LISTP REVERSE U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)|)
69. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U V.REVERSE (U*V)=REVERSE V*REVERSE U|)
71. ∀U V.REVERSE (U*V)=REVERSE V*REVERSE U
deps: NIL
(LINENAME REVERSEAPPEND *)
(COMMENTL LNAME REVERSEAPPEND)
(AXIOM |∀U.REVERSE (REVERSE U)=U|)
73. ∀U.REVERSE (REVERSE U)=U
deps: NIL
(DECL (SUBST) |GROUND⊗GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)|)
75. ∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
deps: NIL
(COMMENTL LNAME DEFINFO)
linenames:
REVERSEAPPEND has line range: (LISPAX#71)
APPENDFACTS has line range: (LISPAX#55 LISPAX#57)
DEFINFO has line range: (LISPAX#53 LISPAX#61 LISPAX#64 LISPAX#69 LISPAX#75)
LISTAPPEND has line range: (LISPAX#51)
SEXPINDUCTION has line range: (LISPAX#35)
LISTINDUCTION has line range: (LISPAX#33)
CONSFACTS has line range: (LISPAX#21 LISPAX#23 LISPAX#29 LISPAX#31)
SIMPINFO has line range: (LISPAX#14 LISPAX#17 LISPAX#21 LISPAX#23 LISPAX#25
LISPAX#27 LISPAX#29 LISPAX#31 LISPAX#40 LISPAX#44
LISPAX#48 LISPAX#55 LISPAX#57)
SORTINFO has line range: (LISPAX#12 LISPAX#14 LISPAX#19 LISPAX#38 LISPAX#42
LISPAX#46 LISPAX#51 LISPAX#67)
the proof LISPAX:
(DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) |GROUND| VARIABLE LISTP)
(DECL (X Y Z) |GROUND| VARIABLE SEXP)
(DECL (A B C) |GROUND| VARIABLE)
(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)
(DECL (NNIL) |GROUND| CONSTANT LISTP)
(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)
(DECL (~) |GROUND⊗GROUND→GROUND| CONSTANT NIL INFIX 850)
(DECL (CAR CDR) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(DECL (ATOM NULL) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(DECL (LISTP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(DECL (SEXP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(AXIOM |∀U.SEXP U|)
12. ∀U.SEXP U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X U.LISTP X~U|)
14. ∀X U.LISTP X~U
deps: NIL
(COMMENTL LNAME SORTINFO SIMPINFO)
(AXIOM |∀U.NULL U≡U=NNIL|)
16. ∀U.NULL U≡U=NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |ATOM NNIL|)
18. ATOM NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |∀U.ATOM U⊃U=NNIL|)
20. ∀U.ATOM U⊃U=NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |NULL NNIL|)
22. NULL NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO NILPROP)
(AXIOM |∀X Y.SEXP X~Y|)
24. ∀X Y.SEXP X~Y
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.¬ATOM X~Y|)
26. ∀X Y.¬ATOM X~Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X U.¬NULL X~U|)
28. ∀X U.¬NULL X~U
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X U.CAR (X~U)=X|)
30. ∀X U.CAR (X~U)=X
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X U.CDR (X~U)=U|)
32. ∀X U.CDR (X~U)=U
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.CAR (X~Y)=X|)
34. ∀X Y.CAR (X~Y)=X
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X Y.CDR (X~Y)=Y|)
36. ∀X Y.CDR (X~Y)=Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))|)
38. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))
deps: NIL
(LINENAME LISTINDUCTION *)
(COMMENTL LNAME LISTINDUCTION)
(AXIOM |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))|)
40. ∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))
deps: NIL
(LINENAME SEXPINDUCTION *)
(COMMENTL LNAME SEXPINDUCTION)
(DECL (LIST) |(GROUND*→GROUND)| FUNCTIONAL)
(AXIOM |∀X.LISTP LIST(X)|)
43. ∀X.LISTP LIST(X)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X.LIST(X)=X~NNIL|)
45. ∀X.LIST(X)=X~NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.LISTP LIST(X,Y)|)
47. ∀X Y.LISTP LIST(X,Y)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.LIST(X,Y)=X~LIST(Y)|)
49. ∀X Y.LIST(X,Y)=X~LIST(Y)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y Z.LISTP LIST(X,Y,Z)|)
51. ∀X Y Z.LISTP LIST(X,Y,Z)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)|)
53. ∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(DECL (*) |(GROUND⊗GROUND*→GROUND)| FUNCTIONAL NIL INFIX 840 BOTH)
(AXIOM |∀U V.LISTP U*V|)
56. ∀U V.LISTP U*V
deps: NIL
(LINENAME LISTAPPEND *)
(COMMENTL LNAME SORTINFO LISTAPPEND)
(AXIOM |∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)|)
58. ∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U.NNIL*U=U|)
60. ∀U.NNIL*U=U
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(AXIOM |∀X U V.X~U*V=X~(U*V)|)
62. ∀X U V.X~U*V=X~(U*V)
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(DECL (ALIST A0 A1 A2) |GROUND| VARIABLE ALISTP)
(AXIOM |∀ALIST.LISTP ALIST|)
65. ∀ALIST.LISTP ALIST
deps: NIL
(COMMENTL LNAME SIMPINFO SORTINFO)
(AXIOM |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)|)
67. ∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)
deps: NIL
(DECL (ASSOC) |GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN NNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALIST ELSE ASSOC(X,CDR ALIST)|)
69. ∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN NNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALIST ELSE ASSOC(X,CDR ALIST)
deps: NIL
(COMMENTL LNAME DEFINFO)
(DECL (MEMBER) |GROUND⊗GROUND→TRUTHVAL| CONSTANT)
(AXIOM |∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))|)
72. ∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))
deps: NIL
(COMMENTL LNAME DEFINFO)
(DECL (REVERSE) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(AXIOM |∀U.LISTP REVERSE U|)
75. ∀U.LISTP REVERSE U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)|)
77. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U V.REVERSE (U*V)=REVERSE V*REVERSE U|)
79. ∀U V.REVERSE (U*V)=REVERSE V*REVERSE U
deps: NIL
(LINENAME REVERSEAPPEND *)
(COMMENTL LNAME REVERSEAPPEND)
(AXIOM |∀U.REVERSE (REVERSE U)=U|)
81. ∀U.REVERSE (REVERSE U)=U
deps: NIL
(LINENAME REVERSEREVERSE *)
(COMMENTL LNAME REVERSEREVERSE)
(DECL (SUBST) |GROUND⊗GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)|)
84. ∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
deps: NIL
(COMMENTL LNAME DEFINFO)
linenames:
REVERSEREVERSE has line range: (LISPAX#81)
REVERSEAPPEND has line range: (LISPAX#79)
APPENDFACTS has line range: (LISPAX#60 LISPAX#62)
DEFINFO has line range: (LISPAX#58 LISPAX#69 LISPAX#72 LISPAX#77 LISPAX#84)
LISTAPPEND has line range: (LISPAX#56)
SEXPINDUCTION has line range: (LISPAX#40)
LISTINDUCTION has line range: (LISPAX#38)
CONSFACTS has line range: (LISPAX#26 LISPAX#28 LISPAX#34 LISPAX#36)
NILPROP has line range: (LISPAX#16 LISPAX#18 LISPAX#20 LISPAX#22)
SIMPINFO has line range: (LISPAX#14 LISPAX#22 LISPAX#26 LISPAX#28 LISPAX#30
LISPAX#32 LISPAX#34 LISPAX#36 LISPAX#45 LISPAX#49
LISPAX#53 LISPAX#60 LISPAX#62 LISPAX#65)
SORTINFO has line range: (LISPAX#12 LISPAX#14 LISPAX#24 LISPAX#43 LISPAX#47
LISPAX#51 LISPAX#56 LISPAX#65 LISPAX#75)
the proof LISPAX:
(DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) |GROUND| VARIABLE LISTP)
(DECL (X Y Z) |GROUND| VARIABLE SEXP)
(DECL (A B C) |GROUND| VARIABLE)
(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)
(DECL (NNIL) |GROUND| CONSTANT LISTP)
(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)
(DECL (~) |GROUND⊗GROUND→GROUND| CONSTANT NIL INFIX 850)
(DECL (CAR CDR) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(DECL (ATOM NULL) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(DECL (LISTP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(DECL (SEXP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(AXIOM |∀U.SEXP U|)
12. ∀U.SEXP U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X U.LISTP X~U|)
14. ∀X U.LISTP X~U
deps: NIL
(COMMENTL LNAME SORTINFO SIMPINFO)
(AXIOM |∀U.NULL U≡U=NNIL|)
16. ∀U.NULL U≡U=NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |ATOM NNIL|)
18. ATOM NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |∀U.ATOM U⊃U=NNIL|)
20. ∀U.ATOM U⊃U=NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |NULL NNIL|)
22. NULL NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO NILPROP)
(AXIOM |∀X Y.SEXP X~Y|)
24. ∀X Y.SEXP X~Y
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.¬ATOM X~Y|)
26. ∀X Y.¬ATOM X~Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X U.¬NULL X~U|)
28. ∀X U.¬NULL X~U
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X U.CAR (X~U)=X|)
30. ∀X U.CAR (X~U)=X
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X U.CDR (X~U)=U|)
32. ∀X U.CDR (X~U)=U
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.CAR (X~Y)=X|)
34. ∀X Y.CAR (X~Y)=X
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X Y.CDR (X~Y)=Y|)
36. ∀X Y.CDR (X~Y)=Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))|)
38. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))
deps: NIL
(LINENAME LISTINDUCTION *)
(COMMENTL LNAME LISTINDUCTION)
(AXIOM |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))|)
40. ∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))
deps: NIL
(LINENAME SEXPINDUCTION *)
(COMMENTL LNAME SEXPINDUCTION)
(DECL (LIST) |(GROUND*→GROUND)| FUNCTIONAL)
(AXIOM |∀X.LISTP LIST(X)|)
43. ∀X.LISTP LIST(X)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X.LIST(X)=X~NNIL|)
45. ∀X.LIST(X)=X~NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.LISTP LIST(X,Y)|)
47. ∀X Y.LISTP LIST(X,Y)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.LIST(X,Y)=X~LIST(Y)|)
49. ∀X Y.LIST(X,Y)=X~LIST(Y)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y Z.LISTP LIST(X,Y,Z)|)
51. ∀X Y Z.LISTP LIST(X,Y,Z)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)|)
53. ∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(DECL (*) |(GROUND⊗GROUND*→GROUND)| FUNCTIONAL NIL INFIX 840 BOTH)
(AXIOM |∀U V.LISTP U*V|)
56. ∀U V.LISTP U*V
deps: NIL
(LINENAME LISTAPPEND *)
(COMMENTL LNAME SORTINFO LISTAPPEND)
(AXIOM |∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)|)
58. ∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U.NNIL*U=U|)
60. ∀U.NNIL*U=U
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(AXIOM |∀X U V.X~U*V=X~(U*V)|)
62. ∀X U V.X~U*V=X~(U*V)
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(DECL (ALIST A0 A1 A2) |GROUND| VARIABLE ALISTP)
(AXIOM |∀ALIST.LISTP ALIST|)
65. ∀ALIST.LISTP ALIST
deps: NIL
(COMMENTL LNAME SIMPINFO SORTINFO)
(AXIOM |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)|)
67. ∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)
deps: NIL
(DECL (ASSOC) |GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN NNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALIST ELSE ASSOC(X,CDR ALIST)|)
69. ∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN NNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALIST ELSE ASSOC(X,CDR ALIST)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀X ALIST.SEXP ASSOC(X,ALIST)|)
71. ∀X ALIST.SEXP ASSOC(X,ALIST)
deps: NIL
(COMMENTL LNAME SORTINFO)
(DECL (MEMBER) |GROUND⊗GROUND→TRUTHVAL| CONSTANT)
(AXIOM |∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))|)
74. ∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))
deps: NIL
(COMMENTL LNAME DEFINFO)
(DECL (REVERSE) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(AXIOM |∀U.LISTP REVERSE U|)
77. ∀U.LISTP REVERSE U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)|)
79. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U V.REVERSE (U*V)=REVERSE V*REVERSE U|)
81. ∀U V.REVERSE (U*V)=REVERSE V*REVERSE U
deps: NIL
(LINENAME REVERSEAPPEND *)
(COMMENTL LNAME REVERSEAPPEND)
(AXIOM |∀U.REVERSE (REVERSE U)=U|)
83. ∀U.REVERSE (REVERSE U)=U
deps: NIL
(LINENAME REVERSEREVERSE *)
(COMMENTL LNAME REVERSEREVERSE)
(DECL (SUBST) |GROUND⊗GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)|)
86. ∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
deps: NIL
(COMMENTL LNAME DEFINFO)
linenames:
REVERSEREVERSE has line range: (LISPAX#83)
REVERSEAPPEND has line range: (LISPAX#81)
APPENDFACTS has line range: (LISPAX#60 LISPAX#62)
DEFINFO has line range: (LISPAX#58 LISPAX#69 LISPAX#74 LISPAX#79 LISPAX#86)
LISTAPPEND has line range: (LISPAX#56)
SEXPINDUCTION has line range: (LISPAX#40)
LISTINDUCTION has line range: (LISPAX#38)
CONSFACTS has line range: (LISPAX#26 LISPAX#28 LISPAX#34 LISPAX#36)
NILPROP has line range: (LISPAX#16 LISPAX#18 LISPAX#20 LISPAX#22)
SIMPINFO has line range: (LISPAX#14 LISPAX#22 LISPAX#26 LISPAX#28 LISPAX#30
LISPAX#32 LISPAX#34 LISPAX#36 LISPAX#45 LISPAX#49
LISPAX#53 LISPAX#60 LISPAX#62 LISPAX#65)
SORTINFO has line range: (LISPAX#12 LISPAX#14 LISPAX#24 LISPAX#43 LISPAX#47
LISPAX#51 LISPAX#56 LISPAX#65 LISPAX#71 LISPAX#77)
the proof LISPAX:
(DECL (U U0 U1 U2 U3 V V0 V1 V2 V3 W W0 W1 W2 W3) |GROUND| VARIABLE LISTP)
(DECL (X Y Z) |GROUND| VARIABLE SEXP)
(DECL (XA YA ZA) |GROUND| VARIABLE ATOM)
(DECL (A B C) |GROUND| VARIABLE)
(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)
(DECL (NNIL) |GROUND| CONSTANT LISTP)
(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)
(DECL (~) |GROUND⊗GROUND→GROUND| CONSTANT NIL INFIX 850)
(DECL (CAR CDR) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(DECL (ATOM NULL) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(DECL (LISTP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(DECL (SEXP) |GROUND→TRUTHVAL| CONSTANT NIL UNARY 750)
(AXIOM |∀U.SEXP U|)
13. ∀U.SEXP U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X U.LISTP X~U|)
15. ∀X U.LISTP X~U
deps: NIL
(COMMENTL LNAME SORTINFO SIMPINFO)
(AXIOM |∀U.NULL U≡U=NNIL|)
17. ∀U.NULL U≡U=NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |ATOM NNIL|)
19. ATOM NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |∀U.ATOM U⊃U=NNIL|)
21. ∀U.ATOM U⊃U=NNIL
deps: NIL
(COMMENTL LNAME NILPROP)
(AXIOM |NULL NNIL|)
23. NULL NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO NILPROP)
(AXIOM |∀X Y.SEXP X~Y|)
25. ∀X Y.SEXP X~Y
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.¬ATOM X~Y|)
27. ∀X Y.¬ATOM X~Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X U.¬NULL X~U|)
29. ∀X U.¬NULL X~U
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X U.CAR (X~U)=X|)
31. ∀X U.CAR (X~U)=X
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X U.CDR (X~U)=U|)
33. ∀X U.CDR (X~U)=U
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.CAR (X~Y)=X|)
35. ∀X Y.CAR (X~Y)=X
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀X Y.CDR (X~Y)=Y|)
37. ∀X Y.CDR (X~Y)=Y
deps: NIL
(COMMENTL LNAME CONSFACTS SIMPINFO)
(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))|)
39. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))
deps: NIL
(LINENAME LISTINDUCTION *)
(COMMENTL LNAME LISTINDUCTION)
(AXIOM |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))|)
41. ∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))
deps: NIL
(LINENAME SEXPINDUCTION *)
(COMMENTL LNAME SEXPINDUCTION)
(DECL (LIST) |(GROUND*→GROUND)| FUNCTIONAL)
(AXIOM |∀X.LISTP LIST(X)|)
44. ∀X.LISTP LIST(X)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X.LIST(X)=X~NNIL|)
46. ∀X.LIST(X)=X~NNIL
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y.LISTP LIST(X,Y)|)
48. ∀X Y.LISTP LIST(X,Y)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y.LIST(X,Y)=X~LIST(Y)|)
50. ∀X Y.LIST(X,Y)=X~LIST(Y)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(AXIOM |∀X Y Z.LISTP LIST(X,Y,Z)|)
52. ∀X Y Z.LISTP LIST(X,Y,Z)
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)|)
54. ∀X Y Z.LIST(X,Y,Z)=X~LIST(Y,Z)
deps: NIL
(COMMENTL LNAME SIMPINFO)
(DECL (*) |(GROUND⊗GROUND*→GROUND)| FUNCTIONAL NIL INFIX 840 BOTH)
(AXIOM |∀U V.LISTP U*V|)
57. ∀U V.LISTP U*V
deps: NIL
(LINENAME LISTAPPEND *)
(COMMENTL LNAME SORTINFO LISTAPPEND)
(AXIOM |∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)|)
59. ∀U V.U*V=IF NULL U THEN V ELSE CAR U~(CDR U*V)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U.NNIL*U=U|)
61. ∀U.NNIL*U=U
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(AXIOM |∀X U V.X~U*V=X~(U*V)|)
63. ∀X U V.X~U*V=X~(U*V)
deps: NIL
(COMMENTL LNAME APPENDFACTS SIMPINFO)
(DECL (ALIST A0 A1 A2) |GROUND| VARIABLE ALISTP)
(AXIOM |∀ALIST.LISTP ALIST|)
66. ∀ALIST.LISTP ALIST
deps: NIL
(COMMENTL LNAME SIMPINFO SORTINFO)
(AXIOM |∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)|)
68. ∀ALIST.¬NULL ALIST⊃¬ATOM CAR ALIST∧ATOM CAR (CAR ALIST)
deps: NIL
(AXIOM |∀XA Y ALIST.ALISTP((XA~Y)~ALIST)|)
69. ∀XA Y ALIST.ALISTP((XA~Y)~ALIST)
deps: NIL
(LINENAME MKALIST *)
(COMMENTL LNAME MKALIST)
(DECL (ASSOC) |GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN NNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALIST ELSE ASSOC(X,CDR ALIST)|)
72. ∀X ALIST.ASSOC(X,ALIST)=
IF NULL ALIST THEN NNIL
ELSE IF X=CAR (CAR ALIST) THEN CAR ALIST ELSE ASSOC(X,CDR ALIST)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀X ALIST.SEXP ASSOC(X,ALIST)|)
74. ∀X ALIST.SEXP ASSOC(X,ALIST)
deps: NIL
(COMMENTL LNAME SORTINFO)
(DECL (MEMBER) |GROUND⊗GROUND→TRUTHVAL| CONSTANT)
(AXIOM |∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))|)
77. ∀X U.MEMBER(X,U)≡¬NULL U∧(X=CAR U∨MEMBER(X,CDR U))
deps: NIL
(COMMENTL LNAME DEFINFO)
(DECL (REVERSE) |GROUND→GROUND| CONSTANT NIL UNARY 950)
(AXIOM |∀U.LISTP REVERSE U|)
80. ∀U.LISTP REVERSE U
deps: NIL
(COMMENTL LNAME SORTINFO)
(AXIOM |∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)|)
82. ∀U.REVERSE U=IF NULL U THEN NNIL ELSE REVERSE (CDR U)*LIST(CAR U)
deps: NIL
(COMMENTL LNAME DEFINFO)
(AXIOM |∀U V.REVERSE (U*V)=REVERSE V*REVERSE U|)
84. ∀U V.REVERSE (U*V)=REVERSE V*REVERSE U
deps: NIL
(LINENAME REVERSEAPPEND *)
(COMMENTL LNAME REVERSEAPPEND)
(AXIOM |∀U.REVERSE (REVERSE U)=U|)
86. ∀U.REVERSE (REVERSE U)=U
deps: NIL
(LINENAME REVERSEREVERSE *)
(COMMENTL LNAME REVERSEREVERSE)
(DECL (SUBST) |GROUND⊗GROUND⊗GROUND→GROUND| CONSTANT)
(AXIOM
|∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)|)
89. ∀X Y Z.SUBST(X,Y,Z)=
IF ATOM Z THEN IF Z=Y THEN X ELSE Z
ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
deps: NIL
(COMMENTL LNAME DEFINFO)
linenames:
REVERSEREVERSE has line range: (LISPAX#86)
REVERSEAPPEND has line range: (LISPAX#84)
MKALIST has line range: (LISPAX#69)
APPENDFACTS has line range: (LISPAX#61 LISPAX#63)
DEFINFO has line range: (LISPAX#59 LISPAX#72 LISPAX#77 LISPAX#82 LISPAX#89)
LISTAPPEND has line range: (LISPAX#57)
SEXPINDUCTION has line range: (LISPAX#41)
LISTINDUCTION has line range: (LISPAX#39)
CONSFACTS has line range: (LISPAX#27 LISPAX#29 LISPAX#35 LISPAX#37)
NILPROP has line range: (LISPAX#17 LISPAX#19 LISPAX#21 LISPAX#23)
SIMPINFO has line range: (LISPAX#15 LISPAX#23 LISPAX#27 LISPAX#29 LISPAX#31
LISPAX#33 LISPAX#35 LISPAX#37 LISPAX#46 LISPAX#50
LISPAX#54 LISPAX#61 LISPAX#63 LISPAX#66)
SORTINFO has line range: (LISPAX#13 LISPAX#15 LISPAX#25 LISPAX#44 LISPAX#48
LISPAX#52 LISPAX#57 LISPAX#66 LISPAX#74 LISPAX#80)